00005	VAR:X;
00010	PRE_PRED:P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19,P20,
00020	P21,P22,P23,P24,P25,P26,P27,P28,P29,
00030	P31,P32,P33,P34,P35,P36,P37,P38,P39,
00040	P41,P42,P43,P44,P45,P46,P47,P48,P49,
00050	P51,P52,P53,P54,P55,P56,P57,P58,P59,
00060	P61,P62,P63,P64,P65,P66,P67,P68,P69,
00070	P71,P72,P73,P74,P75,P76,P77,P78,P79,
00080	P81,P82,P83,P84,P85,P86,P87,P88,P89,
00090	
00092	P91,P92,P93,P94,
00094	P30,P40,P50,P60,P70,P80,P90;
00097	AX:P1∧P2∧P3∧P4⊃(P5∧P6∧P7);
00100	THEOREM:(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((P1∧P2)∧P3)∧P4)⊃((P5∧P6)∧P7))∧~
00200	(((((P8∧P9)∧P2)∧P3)∧P4)⊃P10))∧(((((P11∧P12)∧P2)∧P3)∧P4)⊃P13))∧(((((P14∧P15)∧P2)∧P3)∧P4)⊃P16))∧((((P17∧P18)∧P19)∧~
00300	P20)⊃((P11∧P4)∧P8)))∧(((((P21∧P22)∧P18)∧P19)∧P20)⊃P3))∧(((((P23∧P24)∧P18)∧P19)∧P20)⊃P1))∧(((((P25∧P26)∧P18)∧P19)~
00400	∧P20)⊃P14))∧((((P27∧P28)∧P29)∧P30)⊃((P23∧P21)∧P19)))∧(((((P31∧P32)∧P28)∧P29)∧P30)⊃P20))∧(((((P33∧P12)∧P28)∧P29)∧~
00500	P30)⊃P17))∧(((((P34∧P15)∧P28)∧P29)∧P30)⊃P25))∧((((P35∧P36)∧P37)∧P38)⊃((P34∧P31)∧P30)))∧(((((P39∧P40)∧P36)∧P37)∧P~
00600	38)⊃P29))∧(((((P41∧P22)∧P36)∧P37)∧P38)⊃P27))∧(((((P42∧P43)∧P36)∧P37)∧P38)⊃P33))∧((((P44∧P2)∧P45)∧P46)⊃((P41∧P39)~
00700	∧P38)))∧(((((P47∧P26)∧P2)∧P45)∧P46)⊃P37))∧(((((P48∧P12)∧P2)∧P45)∧P46)⊃P42))∧(((((P49∧P15)∧P2)∧P45)∧P46)⊃P35))∧((~
00800	((P50∧P51)∧P52)∧P53)⊃((P48∧P46)∧P47)))∧(((((P54∧P55)∧P51)∧P52)∧P53)⊃P45))∧(((((P56∧P24)∧P51)∧P52)∧P53)⊃P44))∧(((~
00900	((P57∧P26)∧P51)∧P52)∧P53)⊃P49))∧((((P58∧P59)∧P60)∧P61)⊃((P56∧P54)∧P52)))∧(((((P62∧P63)∧P59)∧P60)∧P61)⊃P53))∧((((~
01000	(P64∧P12)∧P59)∧P60)∧P61)⊃P50))∧(((((P65∧P15)∧P59)∧P60)∧P61)⊃P57))∧(P66⊃P63))∧(P67⊃P68))∧(P69⊃P70))∧(P55⊃P71))∧(P~
01100	40⊃P72))∧(P73⊃P74))∧(P75⊃P9))∧(P76⊃P77))∧(P78⊃P79))∧(P12⊃P24))∧(P80⊃P81))∧(P82⊃P83))∧(P32⊃P84))∧(P15⊃P22))∧(P26⊃~
01200	P43))∧P62)∧P61)∧P60)∧P58)∧P64)∧P65)∧P85)∧P59)∧P28)∧P2)∧P86)∧P51)∧P87)∧P88)∧P18)∧P89)∧P36)∧P90)∧P66)∧P67)∧P69)∧P5~
01300	5)∧P40)∧P73)∧P75)∧P76)∧P78)∧P12)∧P80)∧P82)∧P32)∧P15)∧P26)∧P91)∧P92)∧P93)∧P94)⊃(((P16∧P13)∧P10)∧((P5∧P6)∧P7))
01400	;